Thanks for putting up this PR.

Is it the case that with this change we will never see the IrreducibleLoopException?

If you need to duplicate a node that has invariants, do you duplicate the invariants as well? I suppose yes and that this will happen naturally.

If you need to duplicate a node that has invariants, do you duplicate the invariants as well? I suppose yes and that this will happen naturally.

Yes, in this case the invariant gets copied too. However, we first attempt to duplicate a node that does not have invariants

Thanks for putting up this PR.

Is it the case that with this change we will never see the IrreducibleLoopException?

In the current form, I don't think it can be simply dropped. Actually, this is not the exception that was triggered before by a standard run of boogie on an Irreducible loop:

I managed to trigger it by using the /extractLoops attribute. Specifically, the part where it is thrown is the following:

And caught here (resolved by loop extraction):

The part that I am mostly concerned about is the comment from above: Used by Corral and Dafny.. I believe that one option is to refactor Dafny and Corral to use our implementation of node splitting, but not sure if it's worth it.

The part that I am mostly concerned about is the comment from above: Used by Corral and Dafny.. I believe that one option is to refactor Dafny and Corral to use our implementation of node splitting, but not sure if it's worth it.

ExtractLoops extracts reducible loops into recursive procedures and fails if an irreducible loop is discovered. Is it possible to invoke your new code for making loops reducible within ExtractLoops before doing the extraction into recursive procedures? If yes, then the IrreducibleLoopException should not be thrown.

In general, I would like to take maximal advantage of your impressive PR in Boogie by eliminating all occurrences of

throw new VCGenException("Irreducible flow graphs are unsupported.");

and

throw new IrreducibleLoopException();

If you could do that as part of this PR, great! Otherwise, let us land this PR and hopefully somebody can pick up the remainder of the work later.

If you could do that as part of this PR, great! Otherwise, let us land this PR and hopefully somebody can pick up the remainder of the work later.

This shouldn't be a problem, I will do it in the coming days (shouldn't take long).

In general, I would like to take maximal advantage of your impressive PR in Boogie by eliminating all occurrences of

throw new VCGenException("Irreducible flow graphs are unsupported.");

and

throw new IrreducibleLoopException();

When I first checked the IrreducibleLoopException, I came across this one:

From my understanding, this is part of the Civl infrastructure, thus I assume that in this case the program should be "natively" structured and this piece of code shouldn't be changed. Is this correct?

When I first checked the IrreducibleLoopException, I came across this one:

boogie/Source/Core/AST/Implementation.cs

Lines 634 to 640 in 35aebbe

	else // Proc is YieldProcedureDecl
	{
	graph.ComputeLoops();
	if (!graph.Reducible)
	{
	tc.Error(this, "irreducible control flow graph not allowed");
	}

From my understanding, this is part of the Civl infrastructure, thus I assume that in this case the program should be "natively" structured and this piece of code shouldn't be changed. Is this correct?

Yes, this is part of Civl. But we can change it so that if we discover irreducible loop, we should apply your transformation to make it reducible and then invoke TypecheckLoopAnnotations(tc, graph).

@shazqadeer thank you for the review comments and approval. Would you like me to add/change anything else or shall we land it?

Please go ahead and land the PR.

Unfortunately I don't have push rights on master :)